COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.CENT(MATHEMATICAL THEORIES OF COMPUTATION)
C00008 ENDMK
C⊗;
.CENT(MATHEMATICAL THEORIES OF COMPUTATION)

There is an increasing  body of results dealing with  the more formal
aspects of  of computer science and  programming languages. Since the
very early  days researchers have  examine the  questions of  proving
properites programs: does the program  terminate? does it compute the
desired  function?  is it equivalent  to another given program? is  it
more efficient  in some measure,  than another  program. Some of  the
first  results  can  from  the  efforts  of J.  McCarthy  in  proving
properties of LISP-like programs.  Proof techniques were isolated and
several  non-trivial  results   were  obtained.     The  most  natural
applications  of these methods tend  to be in  proving equivalence of
two algorithmic or procedural specifications. 


Another  branch  of   formalism  grew  up   around  the  problem   of
verification  of programs.  The early  work  of R.  Floyd dealt  with
involving  non-procedural specification. That  is, besides specifying
the algorithm  the program  is  specify %2what%*  is being  computed.
There exist formal ways  of reconciling the %2what%* with the %2how%*
in such a  way that proofs  of correctness and  frequently proofs  of
termination can be obtained.  Later C.A.R. Hoare, inspired by Floyd's
work, attempted  to specify common programming language constructs in
such a  way as to  facilitate such  proofs. He  describes axioms  and
rules of  inference for constuction  of programs. Hoare's  rules form
the  basis  for  several current  verification  systems  and  play an
important part in the structuring of the language PASCAL. 

In the  last five years  another branch  of formalism has  appeared. 
This latest  entry is mostly  due to D.  Scott and appears  under the
name of denotational or mathematical  semantics. The essence here  is
to attempt to reduce  or extact out of an  algorithmic specification,
the fucntion which is being computed. It frequently becomes easier to
prove properties of the underlying function rather than  get involved
with  the particular  algorithm.   This last  area is  the richest  in
mathematical  content, calling on  algebraic and topological notions.
But all three studies involve application of non-trivial mathematics. 

The proposed course  would examine the  above topics and extend  into
related areas in mathematical  logic and recursion theory. The course
is basically a revised version of a summer seminar given at San Jose. 
In that seminar  we covered type-free  lambda calculus and  its model
theory  the typed  lambda calculus and  its applications  to computer
science as the basis for a deductive system for proving properties of
programs.   We  examined  basic logical  systems of  propsitional  and
predicate  calculus, and elementary  number theory; this  lead to the
well-know completeness  and  incompleteness  results and  finally  to
elementary recursion theory. We studied formal models of LISP and the
implications these results had for the field of programming  language
design.  Finally  we   examined  several  implementations   of  these
mathematical  ideas as  practical systems  for proving  properties of
real programs. Similar work would be done in the proposed course. 

The prerequisite  for  the  course is  Math  280 or  consent  of  the
instructor.